STRATEGY =
(LAMBDA (X) (SUPPORT X)) 
SUPPORT-SET-IS: 
¬R(D(U,D(U,D(U,THM57))),D(U,THM57)) 
UNIT-PREFERENCE =NIL
MERGE =NIL
ORDER =NIL
ANCESTRY =T
DEPTH-BOUND =3
LENGTH-BOUND =2

PARMODULATE =T
EQUAL-SYMBOL =R
PAR-DEPTH-BOUND =3
ELAPSED-TIME =80466

NIL 1 2
1 ¬LE(D(U,THM57),D(U,THM57)) 3 10
2 LE(X1,X2) ¬R(D(X1,X2),O) AX 2
3 ¬LE(D(U,THM57),D(U,THM57)) ¬LE(D(U,D(U,THM57)),D(U,D(U,THM57))) 5 8
5 ¬LE(D(U,D(U,D(U,THM57))),D(U,THM57)) ¬LE(D(U,THM57),D(U,THM57)) 7 8
7 ¬LE(D(U,D(U,D(U,THM57))),D(U,THM57)) ¬LE(D(U,D(U,THM57)),THM57) 9 10
8 LE(D(X1,X2),X3) ¬LE(D(X1,X3),X2) HYP 2
9 ¬LE(D(U,THM57),D(U,D(U,D(U,THM57)))) ¬LE(D(U,D(U,D(U,THM57))),D(U,THM57)) 11 12
10 LE(D(X1,X2),D(X1,X3)) ¬LE(X3,X2) HYP 3
11 R(X1,X2) ¬LE(X2,X1) ¬LE(X1,X2) AX 7
12 ¬R(D(U,D(U,D(U,THM57))),D(U,THM57)) THM 1